Definitions | , t T, x:A. B(x), {x:A| B(x)} , x:A B(x), A B, p-open(p), r s, P  Q, False, A, , #$n, FinProbSpace, i j , a < b, Void, -n, n+m, n - m, (i = j), Outcome, {i..j }, Type, x,y:A//B(x;y), RandomVariable(p;n), X Y, SqStable(P), P & Q, type List, x L. P(x), x:A B(x), A c B, True, T, Top, i j < k, ||as||,   , A B, , if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), ,  x,y. t(x;y), s ~ t, {T}, SQType(T), null, <a, b>, f(a), x.A(x), E(n;F), , s = t, S T, suptype(S; T), isint(z;a;b), case b of inl(x) => s(x) | inr(y) => t(y), P  Q, P   Q, i <z j,  b, b, i z j, Unit, left + right, P Q, Dec(P), x:A.B(x), a b,  , (x l),  x. t(x), l[i], a j < b. E(j), rv-shift(x;X), t.2, cons-seq(x;s), t.1 |